$\forall$$i$, $a$:Id, $p$:FinProbSpace, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $P$:(State(${\it ds}$)$\rightarrow\mathbb{B}$).
\\[0ex]@$i$ (with ds: ${\it ds}$ action $a$:$p$ precondition $a$ is $P$ s) $\in$ Dsys